equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
The identity morphism, or simply identity, of an object in some category is the morphism , or , which acts as a two-sided identity for composition.
Given a small category with set of objects and set of morphisms , the identity assigning function of is the function that maps each object in to its identity morphism in .
For the generalisation to an internal category , see identity-assigning morphism.
In Set, the identity morphisms are the identity functions.
Last revised on December 1, 2019 at 08:18:08. See the history of this page for a list of all contributions to it.